PLT-3505 small fixes to the isabelle specification #168
Conversation
palas
force-pushed
the
hrajchert/list-accounts
branch
2 times, most recently
from
a66ce09
to
40274af
Compare
hrajchert
force-pushed
the
hrajchert/scp-3505-small-fixes
branch
2 times, most recently
from
81e76e4
to
2f1fcc7
Compare
| @@ -165,7 +170,7 @@ text \<open>@{thm evalValue_MulValue}\<close> | |||
|
|
|||
| subsubsection \<open>Division\<close> | |||
|
|
|||
| text \<open>Division is a special case because we only evaluate to natural numbers: | |||
| text \<open>Division is a special case because we only evaluate to integers: | |||
There was a problem hiding this comment.
| text \<open>Division is a special case because we only evaluate to integers: | |
| text \<open>Integer division is implemented as follows: |
There was a problem hiding this comment.
This is now obsolete as I am removing Core.thy and rephrasing the whole thing in the refactor Semantic file.
The code/PDF will look like following:
any suggestion will be better made at that PR once it is ready.
| (* TODO: This will become clearer after refactoring the semantics as literal programming PLT-3761 *) | ||
| text \<open>The @{const giveMoney} function is used in @{const reduceContractStep} to execute a Payment. | ||
| It takes as arguments the Party to remove funds from, the Payee to pay to, the amount and token to pay | ||
| and the state accounts. It returns the Payment as a Reduce effect and the new state accounts. |
There was a problem hiding this comment.
Probably not necessary to mention that the accounts are part of the state here
| and the state accounts. It returns the Payment as a Reduce effect and the new state accounts. | |
| and the accounts. It returns the Payment as a Reduce effect and the new accounts. |
There was a problem hiding this comment.
similar note, removing Core.thy. For the moment I'm not even mentioning even the Accounts, moreover, I just give a vague description and a comment that we need to rethink that function
| @@ -1234,5 +1226,5 @@ lemma inputToTransactions_isSingleInput : "isSingleInput (inputsToTransactions s | |||
| lemma traceListToSingleInput_isSingleInput2 : "isSingleInput (traceListToSingleInput t)" | |||
There was a problem hiding this comment.
traceListToSingleInput_isSingleInput2 is unused in the rest of the code base as well
hrajchert
force-pushed
the
hrajchert/scp-3505-small-fixes
branch
from
5694151
to
97fac7d
Compare
TODO: This is marked as a draft until PR 161 has been merged.
This PR adds a changelog starting from the audit and addresses several small findings of the first milestone report.